Nuprl Lemma : flip_wf
4,23
postcript
pdf
k
:
,
i
,
j
:
k
. (
i
,
j
)
k
k
latex
Definitions
(
i
,
j
)
,
if
b
t
else
f
fi
,
i
=
j
,
{
i
..
j
}
,
x
:
A
.
B
(
x
)
,
t
T
,
Lemmas
nat
wf
,
int
seg
wf
,
eq
int
wf
,
ifthenelse
wf
origin
k:
, i, j:k. (i, j) 
k
k k:, i, j:k. (i, j) kk 
t else f fi
j
}x:A. B(x) T